\section{Introduction}

A common kind of concurrency error in shared-memory programs is a
\emph{data race} (or simply race).  The effect of a race is an
incorrect modification of state.  A race occurs when execution
contains two accesses to the same memory location that are not ordered
by the happens-before relation and at least one of the accesses is a
write~\cite{lamport1978}.  Programmers prevent this from happening by
protecting potentially conflicting accesses to shared data with at
least one common lock\Comment{; this discipline assures the accesses
  are ordered}.  Similar to other kinds of concurrency errors, a data
race typically manifests only in certain, rare, thread interleavings
and these interleavings are difficult to reproduce\Comment{; hence it
  is important to help programmers find them}.  To avoid errors
related to the undisciplined use of locks other development methods
and languages~\cite{larus-kozyrakis-cacm2008,yi-ppopp2011} have been
recently proposed and old approaches regained
force~\cite{lauterburg-etal-ase09}.  Irrespective of these advances,
we believe it is important to improve the support for the dominant
programming model that is based on shared-memory.

%% specially considering the increasing demand for software that runs on
%% highly parallel multi-core machines that now became more widespread.

Program model checkers are tools that explore the state-space of
concurrent programs in seek of errors like races and
deadlocks~\cite{godefroid97:model,visser03model,robby03:bogor}.  The
approach is sound (no false positives), but can be very expensive when
searching large state spaces.  We propose \emph{\tname{}} to improve
productivity of model checker users in finding data race errors.  Our
general goal is to enable users to take action in response to race
warnings before a potentially long search for actual errors finishes.
For example, in one of our experiments we ran the \CodeIn{jpapa}
subject (see~Table~\ref{table:main}) in \jpf{}+\tname{} mode, using
depth-search exploration.  After 1m31s of exploration, \tname{}
reports one warning that we confirmed to be an actual manifestation of
race: each warning that \tname{} reports includes information similar
to the one reported by \jpf{} for an actual race.  For this case,
\jpf{} aborts execution after 1h with an ``out of memory error''
message.

%% the object field
%% and for each of the two accesses include the threads involved,
%% location of the access, the kind of access (read or write), and the
%% lock sets involved.  This report is similar to the one given by 

%% One potential conflict consists of a pair of accesses to the same
%% memory location realized by different threads with the use of disjoint
%% lock sets.  We leverage the fact that stateful model checkers keep
%% object and thread ids fixed along the course of state-space
%% exploration.  This enables \tname{} to relate memory accesses that
%% occur across different schedules to predict potential races rapidly.

\Comment{ For the experiments we considered, the model checker
  identifies no distinct memory accesses after \Fix{N}\% of the states
  are visited, on average.}

One important observation to justify our approach is that during
state-space exploration the model checker often covers distinct memory
accesses much sooner than covering the actual race, i.e., sooner than
exploring one particular scheduling that reveals the race. \tname{}
looks for \emph{potential} races \emph{during} state-space exploration
that can be inferred from these accesses.\Comment{ The approach is
  lightweight so to not significantly compromise model checking time
  and space performance to find errors.}  Even though \tname{} ignores
the causality of read and write memory accesses (which can result in
false alarms) and the possibility of loss of object identities (which
can result in race misses), experimental results indicate that it is
precise.  \tname{} \emph{complements} existing explicit-state model
checkers \emph{not} by making it miss less behaviors but by making it
more \emph{responsive}.  Our approach is to anticipate possible
sources of errors before these errors are confirmed (or not).
Similarly to predictive analysis tools like\Comment{BIST~\cite{?},}
Penelope~\cite{sorrentino-fse2010} and
JPredictor~\cite{feng-chen-2008} (see Section~\ref{sec:related}),
\tname{} speculates about alternative thread schedules.  In contrast,
it uses coverage information obtained across the state-space
exploration to infer likely races.  Existing predictive algorithms
consider only one execution trace and applies more expensive analysis
based on that trace.  To the best of our knowledge, this is the first
paper that combines predictive analysis and program model checking and
doing so we introduce a new dimension for predictive analysis:
multiple traces.

This paper makes the following contributions.  

\contr{1}{Idea.}  We propose \tname{}, a novel and lightweight
approach to improve productivity of model checker users in finding
data race errors.  Our approach anticipates likely future reports of
actual errors.\Comment{ \tname{} efficiently collects coverage
  information of observed runs.}

\Comment{ We proposed a technique to optimize model
  checking for a given goal.  The technique operates in two stages:
  one that profiles execution in search of opportunities to reach the
  goal and the other that performs a guided-search}

%% \contr{2}{Application}\Comment{ We instantiated the idea for the
%%   specific context of finding data races in concurrent programs.  In
%%   this context, the profiling stage looks for suspicious accesses to
%%   shared data.  We observed that the profiler obtains precise
%%   information to guide the search and that this information stabilizes
%%   relatively fast}\Fix{...}.
  
\sloppy \contr{2}{Implementations.} We implemented our approach on top
of Java PathFinder~(JPF)~\cite{visser03model} program model checker.

\contr{3}{Experiments.}  We evaluated our approach with \numSubjects{}
subjects from various sources and sizes.  We considered pre-existing
and new errors introduced with volunteers during a study.  Considering
the 28 different scenarios we analyzed, \tname{} reported accurate
warning in less than 5s for 21 cases.  In 13 of these, JPF without
\tname{} takes more than 10min to find the error (9 cases) or runs out
of memory (4 cases).  Results suggest that users can benefit the most
of our approach for large state spaces, the overhead in JPF
exploration time with (unoptimized) \tname{} enabled is on average of
10\%, and that the number of false positives is very low.

\Comment{ We compared \tname{} with depth-first (DFS) and
  breadth-first (BFS) explorations.  For that, we used several
  applications from the Software-artifact Infrastructure Repository
  (SIR)~\cite{doESE05} used previously to evaluate other bug-finding
  techniques.  Our results indicate that \tname{} reduces on average
  the number of states explored by \dfsStateReduction{} in DFS and by
  \bfsStateReduction{} in BFS, on average.  It reduces time by
  \dfsTimeReduction{} in DFS and by \bfsTimeReduction{} in BFS, on
  average}

% LocalWords:  interleavings multi jpapa BIST JPredictor schedules PathFinder
% LocalWords:  JPF pre DFS BFS
